$\forall$${\it ds}$:fpf(Id; $x$.Type\{i\}), ${\it da}$:fpf(Knd; $k$.Type\{i\}), $P$:(ecl(${\it ds}$; ${\it da}$)$\rightarrow$prop\{i':l\}).
\\[0ex]($\forall$$k$:Knd, ${\it test}$:(decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow\mathbb{B}$). $P$(eclbase($k$; ${\it test}$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$,$b$:ecl(${\it ds}$; ${\it da}$). $P$($a$) $\Rightarrow$ $P$($b$) $\Rightarrow$ $P$(eclseq($a$; $b$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$,$b$:ecl(${\it ds}$; ${\it da}$). $P$($a$) $\Rightarrow$ $P$($b$) $\Rightarrow$ $P$(ecland($a$; $b$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$,$b$:ecl(${\it ds}$; ${\it da}$). $P$($a$) $\Rightarrow$ $P$($b$) $\Rightarrow$ $P$(eclor($a$; $b$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$:ecl(${\it ds}$; ${\it da}$). $P$($a$) $\Rightarrow$ $P$(eclrepeat($a$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$:ecl(${\it ds}$; ${\it da}$), $n$:$\mathbb{N}$. $P$($a$) $\Rightarrow$ $P$(eclact($a$; $n$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$:ecl(${\it ds}$; ${\it da}$), $n$:$\mathbb{N}$. $P$($a$) $\Rightarrow$ $P$(eclthrow($a$; $n$)))
\\[0ex]$\Rightarrow$ ($\forall$$a$:ecl(${\it ds}$; ${\it da}$), $l$:($\mathbb{N}$ List). $P$($a$) $\Rightarrow$ $P$(eclcatch($a$; $l$)))
\\[0ex]$\Rightarrow$ guard(($\forall$$x$:ecl(${\it ds}$; ${\it da}$). $P$($x$)))